(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
group3(@l) → group3#1(@l)
group3#1(::(@x, @xs)) → group3#2(@xs, @x)
group3#1(nil) → nil
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y)
group3#2(nil, @x) → nil
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs))
group3#3(nil, @x, @y) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys)
zip3#2(nil, @l3, @x, @xs) → nil
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
zip3#3(nil, @x, @xs, @y, @ys) → nil
Rewrite Strategy: INNERMOST
(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)
Transformed TRS to relative TRS where S is empty.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
group3(@l) → group3#1(@l)
group3#1(::(@x, @xs)) → group3#2(@xs, @x)
group3#1(nil) → nil
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y)
group3#2(nil, @x) → nil
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs))
group3#3(nil, @x, @y) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys)
zip3#2(nil, @l3, @x, @xs) → nil
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
zip3#3(nil, @x, @xs, @y, @ys) → nil
S is empty.
Rewrite Strategy: INNERMOST
(3) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
::/0
group3#2/1
group3#3/1
group3#3/2
tuple#3/0
tuple#3/1
tuple#3/2
zip3#2/2
zip3#3/1
zip3#3/3
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil
S is empty.
Rewrite Strategy: INNERMOST
(5) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
group3(::(::(::(@zs70_0)))) →+ ::(group3(@zs70_0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0].
The pumping substitution is [@zs70_0 / ::(::(::(@zs70_0)))].
The result substitution is [ ].
(6) BOUNDS(n^1, INF)